Nuprl Lemma : remove-repeats_property
11,40
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
L
:(
T
List).
no_repeats(
T
;remove-repeats(
eq
;
L
)) & (
a
:
T
. (
a
remove-repeats(
eq
;
L
))
(
a
L
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
&
Q
,
remove-repeats(
eq
;
L
)
,
t
T
Lemmas
deq
wf
origin
T:Type, eq:EqDecider(T), L:(T List).
a:T. (a 
remove-repeats(eq;L)) 
(a L)) T:Type, eq:EqDecider(T), L:(T List).
a:T. (a remove-repeats(eq;L)) (a L)) x:A. B(x) T